Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	eq(n__0,n__0)	→ true
2:	eq(n__s(X),n__s(Y))	→ eq(activate(X),activate(Y))
3:	eq(X,Y)	→ false
4:	inf(X)	→ cons(X,n__inf(s(X)))
5:	take(0,X)	→ nil
6:	take(s(X),cons(Y,L))	→ cons(activate(Y),n__take(activate(X),activate(L)))
7:	length(nil)	→ 0
8:	length(cons(X,L))	→ s(n__length(activate(L)))
9:	0	→ n__0
10:	s(X)	→ n__s(X)
11:	inf(X)	→ n__inf(X)
12:	take(X1,X2)	→ n__take(X1,X2)
13:	length(X)	→ n__length(X)
14:	activate(n__0)	→ 0
15:	activate(n__s(X))	→ s(X)
16:	activate(n__inf(X))	→ inf(X)
17:	activate(n__take(X1,X2))	→ take(X1,X2)
18:	activate(n__length(X))	→ length(X)
19:	activate(X)	→ X

There are 15 dependency pairs:

The approximated dependency graph contains 2 SCCs: {24-26,29,33,34} and {20}.

Consider the SCC {24-26,29,33,34}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(LENGTH) = π(n__length) = π(s) = 1 together with the lexicographic path order with precedence n__take ≻ TAKE, rule 34 is weakly decreasing and the rules in {24-26,29,33} are strictly decreasing.

Consider the SCC {20}. The usable rules are {4-19}. The constraints could not be solved.

Tyrolean Termination Tool (1.53 seconds) --- May 3, 2006